Nuprl Lemma : send-once-p_wf
11,40
postcript
pdf
T
,
A
:Type,
a
,
x
:Id,
f
:(
A
T
),
tg
:Id,
l
:IdLnk,
es
:event_system{i:l}.
locl(
a
) sends [
tg
,
f
{
A
T
}(
x
)] on link
l
once
prop{i:l}
latex
Definitions
Type
,
t
T
,
Id
,
x
:
A
B
(
x
)
,
IdLnk
,
event_system{i:l}
,
x
:
A
.
B
(
x
)
,
es-E(
es
)
,
s
=
t
,
locl(
a
)
,
left
+
right
,
Knd
,
x
:
A
B
(
x
)
,
P
Q
,
A
c
B
,
guard(
T
)
,
P
Q
,
es-sender(
es
;
e
)
,
let
x
,
y
=
A
in
B
(
x
;
y
)
,
t
.1
,
es-kind(
es
;
e
)
,
es-vartype(
es
;
i
;
x
)
,
b
,
es-when(
es
;
x
;
e
)
,
f
(
a
)
,
es-valtype(
es
;
e
)
,
es-val(
es
;
e
)
,
rcv(
l
,
tg
)
,
x
:
A
.
B
(
x
)
,
source(
l
)
,
prop{i:l}
,
locl(
a
) sends [
tg
,
f
{
A
T
}(
x
)] on link
l
once
Lemmas
lsrc
wf
,
es-valtype
wf
,
rcv
wf
,
es-val
wf
,
subtype
rel
self
,
es-when
wf
,
es-vartype
wf
,
Knd
wf
,
es-kind
wf
,
es-sender
wf
,
es-kind-rcv
,
locl
wf
,
es-E
wf
,
event
system
wf
,
IdLnk
wf
,
Id
wf
origin
T,A:Type, a,x:Id, f:(A
T), tg:Id, l:IdLnk, es:event_system{i:l}.
T}(x)] on link l once 
prop{i:l} T,A:Type, a,x:Id, f:(AT), tg:Id, l:IdLnk, es:event_system{i:l}.
T}(x)] on link l once prop{i:l} 
B(x)
Q
Q
b
x:A. B(x)